/***********************************************************************************************************************
*                                                                                                                      *
* SPLASH build system v0.1                                                                                             *
*                                                                                                                      *
* Copyright (c) 2013 Andrew D. Zonenberg                                                                               *
* All rights reserved.                                                                                                 *
*                                                                                                                      *
* Redistribution and use in source and binary forms, with or without modification, are permitted provided that the     *
* following conditions are met:                                                                                        *
*                                                                                                                      *
*    * Redistributions of source code must retain the above copyright notice, this list of conditions, and the         *
*      following disclaimer.                                                                                           *
*                                                                                                                      *
*    * Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the       *
*      following disclaimer in the documentation and/or other materials provided with the distribution.                *
*                                                                                                                      *
*    * Neither the name of the author nor the names of any contributors may be used to endorse or promote products     *
*      derived from this software without specific prior written permission.                                           *
*                                                                                                                      *
* THIS SOFTWARE IS PROVIDED BY THE AUTHORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED   *
* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL *
* THE AUTHORS BE HELD LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES        *
* (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR       *
* BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT *
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE       *
* POSSIBILITY OF SUCH DAMAGE.                                                                                          *
*                                                                                                                      *
***********************************************************************************************************************/

#include "splashcore.h"

using namespace std;

////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
// Construction / destruction

YosysCrowbarFPGAToolchain::YosysCrowbarFPGAToolchain()
{
	//Get the default compiler path
	m_yosyspath = ShellCommand("which yosys", true);
	if(!DoesFileExist(m_yosyspath))
		FatalError("YosysCrowbarFPGAToolchain: No \"yosys\" binary found");
		
	m_version = ShellCommand("yosys -V");
		
	//Print debug stuff
	DebugPrintfHeading(2, "Initializing Yosys/Crowbar FPGA toolchain...\n");
	DebugPrintfSilent( 3, "    Using %s\n", m_version.c_str());
}

YosysCrowbarFPGAToolchain::~YosysCrowbarFPGAToolchain()
{
	
}

////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
// Accessors

string YosysCrowbarFPGAToolchain::GetDescription() const
{
	return m_version;
}

string YosysCrowbarFPGAToolchain::GetHash() const
{
	return sha256(m_version);
}

string YosysCrowbarFPGAToolchain::GetSynthesisFlagHash(const FPGASynthesisFlagList& flags)
{
	string hashin;
	for(size_t i=0; i<flags.size(); i++)
		hashin += sha256(flags[i]->toString(this));
	return sha256(hashin);
}

string YosysCrowbarFPGAToolchain::GetArchitecture(string device) const
{
	if(device.find("xc2c") == 0)
		return string("xilinx-cpld-cr2-") + device;
	else if(device.find("xc6s") == 0)
		return string("xilinx-fpga-spartan6-") + device;
	else if(device.find("xc7a") == 0)
		return string("xilinx-fpga-artix7-") + device;
	else if(device.find("xc7k") == 0)
		return string("xilinx-fpga-kintex7-") + device;
	else
		FatalError("YosysCrowbarFPGAToolchain: unrecognized device %s\n", device.c_str());
}

////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
// Factories

YosysCrowbarFPGAToolchain* YosysCrowbarFPGAToolchain::CreateDefaultToolchainCached()
{
	if(m_cachedToolchains.find("default_yosys+crowbar") != m_cachedToolchains.end())
		return dynamic_cast<YosysCrowbarFPGAToolchain*>(m_cachedToolchains["default_yosys+crowbar"]);
	return CreateDefaultToolchain();
}

YosysCrowbarFPGAToolchain* YosysCrowbarFPGAToolchain::CreateDefaultToolchain()
{
	YosysCrowbarFPGAToolchain* chain = new YosysCrowbarFPGAToolchain;
	DebugPrintfHeading(2, "Selected default YosysCrowbar FPGA toolchain\n");
	DebugPrintfSilent(2, "    %s\n", chain->GetDescription().c_str());
	m_cachedToolchains["default_yosys+crowbar"] = chain;
	return chain;
}

////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
// Implementation

ClusterJob* YosysCrowbarFPGAToolchain::CompileSourcesToNativeSimulation(
		vector<string> /*source_files*/,
		string /*output_filename*/,
		const vector<ClusterJob*>& /*deps*/,
		string /*top_level*/,
		string /*device*/,
		Cluster* /*cluster*/
		)
{
	FatalError("YosysCrowbarFPGAToolchain::CompileSourcesToNativeSimulation() is not supported\n");
}

ClusterJob* YosysCrowbarFPGAToolchain::SynthesizeSourcesToUnplacedNetlist(
		vector<string> source_files,
		string output_filename,
		const vector<ClusterJob*>& deps,
		string top_level,
		string /*device*/,
		FPGASynthesisFlagList flags,
		Cluster* cluster
		)
{
	//Print the heading
	DebugPrintfHeading(3, "Synthesizing RTLIL netlist file %s\n", output_filename.c_str());
	
	//Get output directory
	string path = GetDirOfFile(output_filename);
	string base = GetBasenameOfFileWithoutExt(output_filename);
	
	//Get the project root directory
	string project_root = CanonicalizePath(path + "/../..");
	
	//Look up includes
	string includes = string("-I ") + project_root + "/generic/include/";
	
	//Check if the flags have any macros
	string macros;
	for(size_t i=0; i<flags.size(); i++)
	{
		FPGASynthesisMacroFlag* mflag = dynamic_cast<FPGASynthesisMacroFlag*>(flags[i]);
		if(mflag == NULL)
			continue;
		macros += string("-D") + mflag->m_name + "=" + mflag->m_value + " ";
	}
	
	//Write the Yosys input script
	string yosys_file = path + "/" + base + ".ys";
	FILE* fp = fopen(yosys_file.c_str(), "w");
	if(!fp)
		FatalError("Failed to create Yosys script file %s\n", yosys_file.c_str());
	fprintf(fp, "#!%s\n", m_yosyspath.c_str());
	fprintf(fp, "\n");
	for(size_t i=0; i<source_files.size(); i++)
		fprintf(fp, "read_verilog -sv %s %s %s\n", includes.c_str(), macros.c_str(), source_files[i].c_str());
	fprintf(fp, "\n");
	fprintf(fp, "hierarchy -top %s -check\n", top_level.c_str());
	fprintf(fp, "\n");
	fprintf(fp, "proc\n");
	fprintf(fp, "opt\n");
	fprintf(fp, "memory\n");
	fprintf(fp, "opt\n");
	fprintf(fp, "\n");
	fprintf(fp, "flatten\n");
	fprintf(fp, "opt\n");
	fprintf(fp, "\n");
	//fprintf(fp, "freduce\n");
	fprintf(fp, "clean\n");
	fprintf(fp, "\n");
	fprintf(fp, "opt\n");
	fprintf(fp, "clean\n");
	/*
	fprintf(fp, "\n");
	fprintf(fp, "fsm_detect\n");
	fprintf(fp, "fsm_extract\n");
	fprintf(fp, "fsm_opt\n");
	fprintf(fp, "opt_clean\n");
	fprintf(fp, "fsm_opt\n");
	fprintf(fp, "fsm_expand\n");
	fprintf(fp, "opt_clean\n");
	fprintf(fp, "fsm_opt\n");
	fprintf(fp, "fsm_recode\n");
	fprintf(fp, "fsm_info\n");
	fprintf(fp, "fsm_export\n");
	fprintf(fp, "fsm_map\n");
	fprintf(fp, "\n");
	//fprintf(fp, "freduce\n");
	//fprintf(fp, "clean\n");
	*/
	fprintf(fp, "\n");
	fprintf(fp, "techmap\n");
	fprintf(fp, "opt\n");
	fprintf(fp, "\n");
	fprintf(fp, "write_ilang %s\n", output_filename.c_str());
	fclose(fp);
		
	//Create the run script
	string runscript = path + "/" + base + "_synthesis_wrapper.sh";
	fp = fopen(runscript.c_str(), "w");
	if(!fp)
		FatalError("Failed to create wrapper script %s\n", runscript.c_str());
	fprintf(fp, "#!/bin/bash\n");
	fprintf(fp, "cd %s\n", path.c_str());
	fprintf(fp, "%s %s\n",
		m_yosyspath.c_str(),
		yosys_file.c_str()
		);
	fprintf(fp, "if [ $? -ne 0 ]; then\n");
	fprintf(fp, "    touch build_failed\n");
	fprintf(fp, "    exit 1\n");
	fprintf(fp, "else\n");
	fprintf(fp, "    touch build_successful\n");
	fprintf(fp, "fi\n");
	fclose(fp);
	if(0 != chmod(runscript.c_str(), 0755))
		FatalError("Failed to set execute permissions on Yosys run script %s\n", runscript.c_str());
	
	//Submit the batch script
	return cluster->SubmitBatchJob(runscript, "yosys", path, deps, 1, 1024);
}

ClusterJob* YosysCrowbarFPGAToolchain::ProveAssertions(
		string input_netlist,
		string testname,
		string path,
		int maxIters,
		const vector< pair<string, string> >& preconditions,
		const vector<string> extra_shows,
		const vector<ClusterJob*>& deps,
		Cluster* cluster
		)
{
	//Print the heading
	DebugPrintfHeading(3, "Proving assertions in RTLIL netlist %s\n", input_netlist.c_str());

	//Get the project root directory
	string project_root = CanonicalizePath(path + "/../..");
	
	//Write the Yosys input script
	string yosys_file = path + "/" + testname + "_proof.ys";
	FILE* fp = fopen(yosys_file.c_str(), "w");
	if(!fp)
		FatalError("Failed to create Yosys script file %s\n", yosys_file.c_str());
	fprintf(fp, "#!%s\n", m_yosyspath.c_str());
	fprintf(fp, "\n");
	fprintf(fp, "read_ilang %s\n", input_netlist.c_str());
	
	//Prove the preconditions
	string precondition_sets;
	for(auto x : preconditions)
	{
		//Run the proof
		fprintf(fp, "sat -tempinduct -seq 1 -verify -prove %s %s %s\n",
			x.first.c_str(),
			x.second.c_str(),
			precondition_sets.c_str());
			
		//Assuming it passes, we'll use this as an assumption for the next proof
		precondition_sets += string("-set ") + x.first + " " + x.second + " ";
	}
	
	//Add extra show commands
	string shows;
	for(auto x : extra_shows)
		shows += string("-show ") + x + " ";
	
	//Format the final show command
	char maxsteps[32] = "";
	if(maxIters != 0)
		snprintf(maxsteps, sizeof(maxsteps), "-maxsteps %d", maxIters);
	fprintf(fp, "sat -tempinduct -seq 1 -prove-asserts -verify -dump_vcd counterexample.vcd -show-inputs %s %s %s\n",
		precondition_sets.c_str(), shows.c_str(), maxsteps);
	fclose(fp);
		
	//Create the run script
	string runscript = path + "/" + testname + "_proof_wrapper.sh";
	fp = fopen(runscript.c_str(), "w");
	if(!fp)
		FatalError("Failed to create wrapper script %s\n", runscript.c_str());
	fprintf(fp, "#!/bin/bash\n");
	fprintf(fp, "cd %s\n", path.c_str());
	fprintf(fp, "%s %s\n",
		m_yosyspath.c_str(),
		yosys_file.c_str()
		);
	fprintf(fp, "if [ $? -ne 0 ]; then\n");
	fprintf(fp, "    echo Proof failed, counterexample at %s/counterexample.vcd\n", path.c_str());
	fprintf(fp, "    touch build_failed\n");
	fprintf(fp, "    exit 1\n");
	fprintf(fp, "else\n");
	fprintf(fp, "    echo Proof successful\n");
	fprintf(fp, "    touch build_successful\n");
	fprintf(fp, "fi\n");
	fclose(fp);
	if(0 != chmod(runscript.c_str(), 0755))
		FatalError("Failed to set execute permissions on Yosys run script %s\n", runscript.c_str());
	
	//Submit the batch script
	return cluster->SubmitBatchJob(runscript, "yosys", path, deps, 1, 8192);
}

ClusterJob* YosysCrowbarFPGAToolchain::PlaceAndRouteNetlist(
		string /*input_netlist*/,
		string /*constraints*/,
		string /*output_filename*/,
		string /* device */,
		const vector<ClusterJob*>& /*deps*/,
		FPGAPlaceAndRouteFlagList /*flags*/,
		Cluster* /*cluster*/
		)
{
	FatalError("YosysCrowbarFPGAToolchain::PlaceAndRouteNetlist() not implemented\n");
}

ClusterJob* YosysCrowbarFPGAToolchain::StaticTimingAnalysis(
		string /*input_netlist*/,
		string /*constraints*/,
		string /*output_filename*/,
		int /*speedgrade*/,
		const vector<ClusterJob*>& /*deps*/,
		FPGATimingAnalysisFlagList /*flags*/,
		Cluster* /*cluster*/
		)
{
	FatalError("YosysCrowbarFPGAToolchain::StaticTimingAnalysis() not implemented\n");
}

ClusterJob* YosysCrowbarFPGAToolchain::GenerateBitstream(
		string /*input_netlist*/,
		string /*constraints*/,
		string /*output_filename*/,
		string /*device*/,
		const vector<ClusterJob*>& /*deps*/,
		FPGABitstreamGenerationFlagList /*flags*/,
		Cluster* /*cluster*/
		)
{
	FatalError("YosysCrowbarFPGAToolchain::GenerateBitstream() not implemented\n");
}

ClusterJob* YosysCrowbarFPGAToolchain::FitCPLDNetlist(
		string /*input_netlist*/,
		string /*output_filename*/,
		string /*device*/,
		const vector<ClusterJob*>& /*deps*/,
		Cluster* /*cluster*/
		)
{
	FatalError("YosysCrowbarFPGAToolchain::FitCPLDNetlist() not implemented\n");
}

ClusterJob* YosysCrowbarFPGAToolchain::GenerateCPLDBitstream(
		string /*input_netlist*/,
		string /*output_filename*/,
		const vector<ClusterJob*>& /*deps*/,
		Cluster* /*cluster*/
		)
{
	FatalError("YosysCrowbarFPGAToolchain::GenerateCPLDBitstream() not implemented\n");
}

////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
// Flags
